l:IdLnk, dt:tg:Id fp Type, knd:Knd, T:Type.
(isrcv(knd)  lnk(knd) = l  tag(knd)  dom(dt)  T = dt(tag(knd)))
 lnk-decl(l;dt) || knd : T 

latex

Definitions	Knd, Type, lnk-decl(l;dt), f(x), <a,b>, s = t, P  Q, t  T, {T}, x:A. B(x), SQType(T), Prop, s ~ t, left+right, Void, x:A. B(x), Top, KindDeq, x:AB(x), x:AB(x), P & Q, P  Q, x. t(x), a:A fp B(a), x.A(x), x : v, x  dom(f), b, f || g, IdLnk, Id, tag(k), IdDeq, lnk(k), a = b, isrcv(k), rcv(l,tg), 1of(t), map(f;as), type List, x:A. B(x), True, P  Q, Dec(P), False, P  Q, A
Lemmas	assert-eq-lnk, decidable assert, member map, map wf, rcv wf, assert-deq-member, isrcv wf, eq lnk wf, lnk wf, fpf-ap wf, id-deq wf, tagof wf, Id wf, IdLnk wf, assert wf, fpf-dom wf, fpf-single wf, fpf-trivial-subtype-top, lnk-decl wf, fpf wf, top wf, fpf-single-dom, Kind-deq wf, Knd wf, Knd sq